/* Copyright 2013 Nicola Olivetti, Gian Luca Pozzato. This file is part of NESCOND.NESCOND is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with NESCOND. If not, see . */ CK+ID (a1 => (a1 -> p)) -> (a1 => p) (a1 => (a1 -> (a2 => (a2 -> p)))) -> (a1 => (a2 => p)) (a1 => (a1 -> (a2 => (a2 -> (a3 => (a3 -> p)))))) -> (a1 => (a2 => (a3 => p))) (a1 => (a1 -> (a2 => (a2 -> (a3 => (a3 -> (a4 => (a4 -> p)))))))) -> (a1 => (a2 => (a3 => (a4 => p)))) (a1 => (a1 -> (a2 => (a2 -> (a3 => (a3 -> (a4 => (a4 -> (a5 => (a5 -> (a6 => (a6 -> p)))))))))))) -> (a1 => (a2 => (a3 => (a4 => (a5 => (a6 => p)))))) ((a => b1) ^ (a => b2)) => (a => (b1 ^ b2)) ((a => b1) ^ (a => b2) ^ (a => b3)) => (a => (b1 ^ b2 ^ b3)) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ) => (a => (b1 ^ b2 ^ b3 ^ b4)) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5)) => (a => (b1 ^ b2 ^ b3 ^ b4 ^b5)) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6)) => (a => (b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6)) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7)) => (a => (b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7)) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8)) => (a => (b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8)) CK+MP (a => b1) -> (a -> b1) (((a => b1) -> (a -> b1)) => b2) -> b2 (((((a => b1) -> (a -> b1)) => b2) -> b2) => b3) -> b3 (((((((a => b1) -> (a -> b1)) => b2) -> b2) => b3) -> b3) => b4) -> b4 (((((((((a => b1) -> (a -> b1)) => b2) -> b2) => b3) -> b3) => b4) -> b4) => b5) -> b5 ((a => b) ^ (!a => b)) -> b (((p ^ q) => c) ^ (((!p) ^ q) => c) ^ ((p ^ (!q)) => c) ^ (((!p) ^ (!q)) => c)) -> c CK+ID+MP ((a => a) => b) -> b (a => b) => (a -> b) (((a => b) => (a -> b)) => c) -> c (a => (a => b)) -> (a => b) (a => (a => (a => b))) -> (a => b) (a => (a => (a => (a => b)))) -> (a => b) (a => (a => (a => (a => (a => b))))) -> (a => b) (a => (a => (a => (a => (a => (a => b)))))) -> (a => b) (a => (a => (a => (a => (a => (a => (a => b))))))) -> (a => b) (a => (a => (a => (a => (a => (a => (a => (a => b)))))))) -> (a => b) CEM (a1 => (a2 => (b1 v b2))) -> ((a1 => (a2 => b1)) v (a1 => (a2 => b2))) (a1 => (a2 => (a3 => (b1 v b2)))) -> ((a1 => (a2 => (a3 => b1))) v (a1 => (a2 => (a3 => b2)))) (a1 => (a2 => (a3 => (a4 => (b1 v b2))))) -> ((a1 => (a2 => (a3 => (a4 => b1)))) v (a1 => (a2 => (a3 => (a4 => b2))))) (a1 => (a2 => (a3 => (a4 => (a5 => (b1 v b2)))))) -> ((a1 => (a2 => (a3 => (a4 => (a5 => b1))))) v (a1 => (a2 => (a3 => (a4 => (a5 => b2)))))) (a1 => (a2 => (a3 => (a4 => (a5 => (a6 => (b1 v b2))))))) -> ((a1 => (a2 => (a3 => (a4 => (a5 => (a6 => b1)))))) v (a1 => (a2 => (a3 => (a4 => (a5 => (a6 => b2))))))) (a => (b1 v b2)) -> ((a => b1) v (a => b2)) (a => (b1 v b2 v b3)) -> ((a => b1) v (a => b2) v (a =>b3)) (a => (b1 v b2 v b3 v b4)) -> ((a => b1) v (a => b2) v (a => b3) v (a => b4)) (a => (b1 v b2 v b3 v b4 v b5)) -> ((a => b1) v (a => b2) v (a => b3) v (a => b4) v (a => b5)) (a => (b1 v b2 v b3 v b4 v b5 v b6)) -> ((a => b1) v (a => b2) v (a => b3) v (a => b4) v (a => b5) v (a => b6)) (a => (b1 v b2 v b3 v b4 v b5 v b6 v b7)) -> ((a => b1) v (a => b2) v (a => b3) v (a => b4) v (a => b5) v (a => b6) v (a => b7)) (a => (b1 v b2 v b3 v b4 v b5 v b6 v b7 v b8)) -> ((a => b1) v (a => b2) v (a => b3) v (a => b4) v (a => b5) v (a => b6) v (a => b7) v (a => b8)) ((a => (b1 v b2)) => c) -> (((a => b1) v (a => b2)) => c) CEM+ID (a1 => (a1 -> (b1 v b2))) => ((a1 => b1) v (a1 => b2)) (a1 => (a1 -> (a2 => (a2 -> (b1 v b2 v b3))))) => ((a1 => (a2 => b1)) v (a1 => (a2 => b2)) v (a1 => (a2 => b3))) (a1 => (a1 -> (a2 => (a2 -> (a3 => (a3 -> (b1 v b2 v b3 v b4))))))) => ((a1 => (a2 => (a3 => b1))) v (a1 => (a2 => (a3 => b2))) v (a1 => (a2 => (a3 => b3)))) (a => (b1 v b2)) => ((a => b1) v (a => b2)) (a => (b1 v b2 v b3)) => ((a => b1) v (a => b2) v (a =>b3)) (a => (b1 v b2 v b3 v b4)) => ((a => b1) v (a => b2) v (a => b3) v (a => b4)) (a => (b1 v b2 v b3 v b4 v b5)) => ((a => b1) v (a => b2) v (a => b3) v (a => b4) v (a => b5)) (a => (b1 v b2 v b3 v b4 v b5 v b6)) => ((a => b1) v (a => b2) v (a => b3) v (a => b4) v (a => b5) v (a => b6)) (a => (b1 v b2 v b3 v b4 v b5 v b6 v b7)) => ((a => b1) v (a => b2) v (a => b3) v (a => b4) v (a => b5) v (a => b6) v (a => b7)) (a => (b1 v b2 v b3 v b4 v b5 v b6 v b7 v b8)) => ((a => b1) v (a => b2) v (a => b3) v (a => b4) v (a => b5) v (a => b6) v (a => b7) v (a => b8)) CSO (= CK+ID+CSO): ((a => b1) ^ (a => c)) -> ((a ^ b1) => c) ((a => b1) ^ (a => b2) ^ (a => c)) -> ((a ^ b1 ^ b2) => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3) => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4) => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5) => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6) => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7) => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8) => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ (a => b9) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 ^ b9) => c) ((a => b1) ^ ((a ^ b1) => c)) -> (a => c) ((a => b1) ^ (a => b2) ^ ((a ^ b1 ^ b2) => c)) -> (a => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ ((a ^ b1 ^ b2 ^ b3) => c)) -> (a => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4) => c)) -> (a => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5) => c)) -> (a => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6) => c)) -> (a => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7) => c)) -> (a => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8) => c)) -> (a => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ (a => b9) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 ^ b9) => c)) -> (a => c) ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ (a => b9) ^ (a => b10) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 ^ b9 ^ b10) => c)) -> (a => c) ((a1 => a2) ^ (a2 => a1) ^ (a1 => c)) -> (a2 => c) ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a1 => c)) -> (a3 => c) ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a1 => c)) -> (a4 => c) ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a4 => a5) ^ (a5 => a4) ^ (a1 => c)) -> (a5 => c) ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a4 => a5) ^ (a5 => a4) ^ (a5 => a6) ^ (a6 => a5) ^ (a1 => c)) -> (a6 => c) ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a4 => a5) ^ (a5 => a4) ^ (a5 => a6) ^ (a6 => a5) ^ (a6 => a7) ^ (a7 => a6) ^ (a1 => c)) -> (a7 => c) ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a4 => a5) ^ (a5 => a4) ^ (a5 => a6) ^ (a6 => a5) ^ (a6 => a7) ^ (a7 => a6) ^ (a7 => a8) ^ (a8 => a7) ^ (a1 => c)) -> (a8 => c)